i, x, a:Id, A, T:Type, x0:A, P:(ATProp). R-pre-init1(i;x;A;x0;a;T;P)  Realizer 

latex

Definitions

Id, x : v, t  T, Void, f(x)?z, a:A fp B(a), b, P  Q, x:AB(x), x:A. B(x), {x:A| B(x) }, Top, Type, x:A. B(x), x.A(x), x. t(x), State(ds), IdDeq, f(a), R-pre-init(i;ds;init;a;T;P), R-pre-init1(i;x;A;x0;a;T;P), Prop, P & Q, True, eqof(d), true, A, b, x:AB(x), p  q, , s = t, false, False, left+right, P  Q, p  q, P  Q, P  Q, T, Unit, f(x), x  dom(f)

Lemmas

iff wf, fpf-dom wf, fpf-trivial-subtype-top, eqtt to assert, assert of bor, eqff to assert, squash wf, bnot thru bor, iff transitivity, assert of band, and functionality wrt iff, assert of bnot, bor wf, false wf, bfalse wf, bool wf, band wf, bnot wf, not wf, assert wf, btrue wf, eqof wf, true wf, subtype rel self, R-pre-init wf, fpf-cap-single1, id-deq wf, top wf, decl-state wf, fpf-single wf, Id wf